﻿/************************************************************************
 * AIDE - Automata Identification Engine
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     AIDE\OnlineAlgo\NFMs\L_Plus_M.cs
 * Description  :     Implementation of Shahbaz Learnin Algorithm (called L plus M)
 * Change log   :     -20 Dec 2012:  First version
 *                    -5  May 2013:  Added the initialization with a model to make it capable of adaptive model checking
 *                    -6  May 2013:  Method AddSuffix added
 * 					  -6 June 2014:	 Add "ExportObservationTable" feature
 * 					  -16 March 2015: check closeness after adding each suffix
 * To Do        :     -Test/Debug it for incomplete machines
 * 					  -Optimize the code
 ************************************************************************/
//TODO : implement this!
//#define SUPPORT_NOT_INPUTENABLED_MM
using System;
using System.Collections.Generic;
using AIDE.Base;
using MBT.GraphAlgorithms;
using SMLib.Automata.Base;
using SMLib.Automata.MM;
using AIDE.Oracles.NFMs;

namespace AIDE.OnlineAlgo.NFMs
{
	/// <summary>
	/// Shahbaz Algorithm L+m : Learner
	/// <remarks>Based on [Muzammil Shahbaz - Reverse Engineering Enhanced States Models of Black Box Software 
	/// Components to support Integration Testing (PhD Thesis-2008): page 68]</remarks>
	/// </summary>
	public class L_Plus_M: INFM_Learner
	{
		/// <summary>
		/// Alphabet
		/// </summary>
		protected Alphabet InputAlphabet;
		protected IOracle_MAT_MM myOracle;

		protected int phase;
		#region ObservationTable
		/// <summary>
		/// SD AND ED be the non-empty finite sets of finite strings over SigMa. 
		/// SD is a prefix-closed set 
		/// </summary>
		protected List<TD_Row> Sm;
		protected List<TD_Row_Parrented> Sm_I;
		/// <summary>
		/// Em is a suffix-closed set of strings.
		/// </summary>
		protected List<Word> Em;
		#region observation table row
		protected class TD_Row
		{
			public Word accessString;
			/// <summary>
			/// outputs
			/// </summary>
			public List<Word> Em_Row;
			public int generatedStateIndex;

			/// <summary>
			/// Constructor
			/// </summary>
			public TD_Row ()
			{
				accessString = new Word ();
				Em_Row = new List<Word> ();
				generatedStateIndex = -1;
			}

			/// <summary>
			/// Copy constructor
			/// </summary>
			/// <param name="r"></param>
			/// <param name="op"></param>
			public TD_Row (TD_Row r, Word op = null)
			{
				generatedStateIndex = -1;

				if (op == null)
					accessString = new Word (r.accessString);
				else
					accessString = new Word (op);

				Em_Row = new List<Word> ();
				//for (int i = 0; i < r.Em_Row.Count; i++)
				//	Em_Row.Add (r.Em_Row [i]);
			}

			/// <summary>
			/// Assume that the lenght of two rows are the same
			/// </summary>
			/// <param name="anotherRow"></param>
			/// <returns></returns>
			public int FirstDifference (TD_Row t)
			{
				for (int i = 0; i < Em_Row.Count; i++) {
					//* to support input-incompletness!
					if (Em_Row [i] == null && t.Em_Row [i] == null)
						continue;
					else if (Em_Row [i] == null || t.Em_Row [i] == null)
						return i;
					
					if (!Em_Row [i].Equals (t.Em_Row [i])) 
						return i;
				}
				return -1;
			}

			/// <summary>
			/// If this row is same as another
			/// </summary>
			/// <param name="anotherRow"></param>
			/// <returns></returns>
			public bool HasSameRow (TD_Row t)
			{
				return FirstDifference (t) == -1;
			}

			public override string ToString ()
			{
				string st = "";
				for (int i = 0; i < Em_Row.Count; i++)
					st += (Em_Row [i] == null ? "NULL" : Em_Row [i].ToString ());
				return accessString.ToString () + st;
			}
		}

		protected class TD_Row_Parrented : TD_Row
		{
			public TD_Row parent;

			public TD_Row_Parrented (TD_Row t, Word p = null)
                : base(t, p)
			{
				parent = t;
			}

			public TD_Row_Parrented ()
                : base()
			{
				parent = null;
			}
		}
		#endregion
		/// <summary>
		/// Fills a row
		/// </summary>
		/// <param name="row">Row</param>
		protected void FillRow (TD_Row row)
		{
			foreach (Word w in Em) {
				Word tmp = w.Clone ();
				LearningLog.LogStartMQ ();
				Word output = myOracle.OutputTrace (row.accessString, tmp);
				LearningLog.LogFinishMQ ();

				if (output == null)
					row.Em_Row.Add (null);
				else                    	
					row.Em_Row.Add (output.Suffix (w.Length));
			}
		}

		/// <summary>
		/// Initialize the observation table
		///    Let TD be a finite function that maps (SD union SD.Sigma)* ED to {0; 1}
		///    An observation table (Sm,Em,Tm) can be visualized as a two-dimensional array with rows labeled by the elements of
		///    SD union SD.Sigma AND columns labeled by the elements of ED, with the entry for a row input in 
		///    SD union SD.Sigma AND a column e 2 ED equals to TD(input; e).
		/// </summary>
		void InitializeObservationTable ()
		{
			Sm = new List<TD_Row> ();
			Sm_I = new List<TD_Row_Parrented> ();
			Em = new List<Word> ();

			//1- Em=I
			foreach (ISymbol symb in InputAlphabet.AllSymbols()) {
				Word eps = new Word ();
				eps.AddSymbol (symb);
				Em.Add (eps);
			}

			//2- Sm={""}
			TD_Row r = new TD_Row ();
			r.accessString = new Word ();
			Sm.Add (r);
			FillRow (r);

			//* 3- add all words of Sigma into Sm_I
			foreach (TD_Row row in Sm) {
				int indexOfSym = 0;
				//* it is always just Epsilon, but if the learning starts with a model, it will have more access string!
				foreach (ISymbol symb in InputAlphabet.AllSymbols()) {
					
					//* to support output incompletness!
					indexOfSym++;
					if (row.Em_Row [indexOfSym - 1] == null) {
						continue;	
					}
					
					TD_Row_Parrented r2 = new TD_Row_Parrented ();
					r2.parent = row;
					r2.accessString.AddWord (row.accessString);
					r2.accessString.AddSymbol (symb);

					//* add just if the row is not already in Sm_I
					//if (indexOfPath (Sm_I, r2.accessString) >= 0)
					//	continue;					
					
					Sm_I.Add (r2);
					FillRow (r2);
				}
			}
		}

		/// <summary>
		/// To add another suffix, we need to add a column into the observation table.
		/// By default, this suffix leads to a non-accepting state for all prefixes.
		/// Afterward, we need to update it by trying to call membership query.
		/// </summary>
		protected void AddColumn ()
		{
			foreach (TD_Row t in Sm) {
				t.Em_Row.Add (/*new Word ()*/null);//a cell for output
			}
			foreach (TD_Row t in Sm_I) {
				t.Em_Row.Add (/*new Word ()*/null);//a cell for output
			}
		}

		/// <summary>
		/// Check that the observation table is closed myOracle not
		/// </summary>
		/// <returns>
		/// -1: the observation table is Closed
		/// i : the first row number of Sm.Sigma that makes the table un-closed
		/// </returns>
		protected int isClosed ()
		{
			for (int i = 0; i < Sm_I.Count; i++) {
				TD_Row t = Sm_I [i];
				bool found = false;
				foreach (TD_Row r in Sm) {
					if (r.HasSameRow (t)) {
						found = true;
						break;
					}
				}
				//* there is no equivalent row in Sm corresponding to this Sm_I row
				if (!found) 
					return i;
			}
			//* the table is closed
			return -1;
		}

		enum ExportOptions
		{
			XML,
			CSV,
			HTML}
		;

		ExportOptions exportFormat;
		protected bool exportTables, exportConj;

		/// <summary>
		/// Prints the table into XML format (for debbugging use) into 
		/// "Table+phase.xml" in the working directory
		/// </summary>
		protected void ExportObservationTable ()
		{
			exportFormat = ExportOptions.HTML;
			if (exportFormat == ExportOptions.XML) {
				System.Text.StringBuilder sb = new System.Text.StringBuilder ();
				sb.AppendLine ("<table phase=\"" + phase + "\">");
				for (int i=0; i<(this.Sm.Count+this.Sm_I.Count); i++) {
					sb.Append ("<row accessSequence=\"");
					if (i < Sm.Count)
						sb.AppendLine (Sm [i].accessString + "\" of=\"Sm\">");
					else
						sb.AppendLine (Sm_I [i - Sm.Count].accessString + "\" of=\"Sm_I\">");
				

					for (int j=0; j<Em.Count; j++) {
						sb.AppendLine ("<cell column=\"" + j + "\" header=\"" + Em [j].ToString () + "\">");
						if (i < Sm.Count) {
							string st = (Sm [i].Em_Row [j] == null) ? "-" : Sm [i].Em_Row [j].ToString ();
							sb.AppendLine (st.ToString ());
						} else {
							string st = (Sm_I [i - Sm.Count].Em_Row [j] == null) ? "-" : Sm_I [i - Sm.Count].Em_Row [j].ToString ();
							sb.AppendLine (st.ToString ());
						}
						sb.AppendLine ("</cell>");					
					}
					sb.AppendLine ("</row>");
				}
				sb.AppendLine ("</table>");
				System.IO.File.WriteAllText (LibSetting.WorkingPath + "Table" + this.phase + ".xml",
				                             sb.ToString ());
			} else if (exportFormat == ExportOptions.HTML) {
				System.Text.StringBuilder sb = new System.Text.StringBuilder ();
				sb.AppendLine ("<html><body>Observation table (phase " + phase + ")<table border=\"1\">");
				sb.Append ("<tr><th><b>Access Sequence</th>");				
				for (int j=0; j<Em.Count; j++)
					sb.Append ("<th>" + Em [j] + "</th>");
				sb.Append ("</tr>");
				
				for (int i=0; i<(this.Sm.Count+this.Sm_I.Count); i++) {
					if (i < Sm.Count) 
						sb.Append ("<tr><td bgcolor=\"#BEE6B8\">");
					else
						sb.Append ("<tr><td bgcolor=\"#EDD5A8\">");
					
					if (i < Sm.Count)
						sb.Append (Sm [i].accessString + "</td>");
					else
						sb.Append (Sm_I [i - Sm.Count].accessString + "</td>");
				

					for (int j=0; j<Em.Count; j++) {
						sb.Append ("  <td>");
						if (i < Sm.Count) {
							string st = (Sm [i].Em_Row [j] == null) ? "-" : Sm [i].Em_Row [j].ToString ();
							sb.Append (st.ToString ());
						} else {
							string st = (Sm_I [i - Sm.Count].Em_Row [j] == null) ? "-" : Sm_I [i - Sm.Count].Em_Row [j].ToString ();
							sb.Append (st.ToString ());
						}
						sb.AppendLine ("</td>");					
					}
					sb.AppendLine ("</tr>");
				}
				sb.AppendLine ("</body></html>");
				System.IO.File.WriteAllText (LibSetting.WorkingPath + "Table" + this.phase + ".html",
				                             sb.ToString ());
			} else if (exportFormat == ExportOptions.CSV) {
				System.Text.StringBuilder sb = new System.Text.StringBuilder ();
				sb.Append ("Access Sequence");				
				for (int j=0; j<Em.Count; j++)
					sb.Append (", " + Em [j]);
				sb.AppendLine ();
				
				for (int i=0; i<(this.Sm.Count+this.Sm_I.Count); i++) {
					if (i < Sm.Count)
						sb.Append (Sm [i].accessString + ", ");
					else
						sb.Append (Sm_I [i - Sm.Count].accessString + ", ");
				
					for (int j=0; j<Em.Count; j++) {
						if (i < Sm.Count) {
							string st = (Sm [i].Em_Row [j] == null) ? " " : Sm [i].Em_Row [j].ToString ();
							sb.Append (st.ToString ());
						} else {
							string st = (Sm_I [i - Sm.Count].Em_Row [j] == null) ? " " : Sm_I [i - Sm.Count].Em_Row [j].ToString ();
							sb.Append (st.ToString ());
						}
						sb.Append (",");					
					}
					sb.AppendLine ("");
				}
				System.IO.File.WriteAllText (LibSetting.WorkingPath + "Table" + this.phase + ".csv",
				                             sb.ToString ());
			}
		}

		/// <summary>
		/// Build the conjecture automata based on observation table
		/// </summary>
		/// <returns>
		/// the generated automata
		/// </returns>
		protected MealyMachine BuildConjecture ()
		{
			MealyMachine conj = new MealyMachine ();
			MealyMachine.Mealy_State currentState;
			MealyMachine.Mealy_Transition tr;

			int currentRowIndex = 0;
			Word p;
			TD_Row currentRow;

			//* rows that are converted to state
			List<TD_Row> statedRow = new List<TD_Row> ();
			
			//* generate all states
			for (int y = 0; y < Sm.Count; y++) {
				conj.AddState (new MealyMachine.Mealy_State (y.ToString ()));
				statedRow.Add (Sm [y]);
			}

			currentRow = Sm [0];

			//* generate states breast first order
			for (currentRowIndex = 0; currentRowIndex < statedRow.Count; currentRowIndex++) {
				currentRow = statedRow [currentRowIndex];
				currentState = (MealyMachine.Mealy_State)conj [currentRowIndex];
				
				int indexOfSym = 0;
				foreach (ISymbol s in InputAlphabet.AllSymbols()) {
					
					//* to support output incompletness!
					indexOfSym++;
					if (currentRow.Em_Row [indexOfSym - 1] == null) {
						continue;
					}
					
					p = new Word (currentRow.accessString);
					p.AddSymbol (s);
					bool nextRowFound = false;
					//* find next row in Sm
					for (int i = 1; i < Sm.Count; i++) {
						if (Sm [i].accessString.Equals (p)) {
							//* Found!
							nextRowFound = true;

							//* find that this row exists in the generated states?
							for (int j = 0; j < statedRow.Count; j++) {
								TD_Row r = statedRow [j];
								if (r.HasSameRow (Sm [i])) {
									//* generate transition to this state from current state
									//* first: find the output
									Word tmp = new Word (s);
									ISymbol output = null;
									for (int iii = 0; iii < InputAlphabet.Size; iii++) {
										if (Em [iii].Equals (tmp)) {
											//* to support output incompletness!
											if (currentRow.Em_Row [iii] == null)
												output = null;
											else
												
												output = currentRow.Em_Row [iii].GetSymByIndex (0);
											break;
										}
									}
									//* to support output incompletness!
									if (output != null) {
										tr = new MealyMachine.Mealy_Transition (s, output);

										tr.SetDestination ((MealyMachine.Mealy_State)conj [j]);
										currentState.Transitions.Add (tr);
									}
									break;
								}
							}
							break;
						}
					}
					if (nextRowFound)
						continue;

					//* not found in Sm? No problem. So find next row in Sm_I:
					for (int i = 0; i < Sm_I.Count; i++) {
						if (Sm_I [i].accessString.Equals (p)) {
							
							//* find that this row exists in the generated states?
							for (int j = 0; j < statedRow.Count; j++) {
								TD_Row r = statedRow [j];
								if (r.HasSameRow (Sm_I [i])) {
									//* generate transition to this state from current state
									nextRowFound = true;
									//* first: find the output
									Word tmp = new Word (s);
									ISymbol output = null;
									for (int iii = 0; iii < InputAlphabet.Size; iii++) {
										if (Em [iii].Equals (tmp)) {
											//* to support output incompletness!
											if (currentRow.Em_Row [iii] == null)
												output = null;
											else
												
												output = currentRow.Em_Row [iii].GetSymByIndex (0);
											break;
										}
									}
									
									//* to support output incompletness!
									if (output != null) {
										tr = new MealyMachine.Mealy_Transition (s, output);
										tr.SetDestination ((MealyMachine.Mealy_State)conj.GetStates () [j]);
										currentState.Transitions.Add (tr);
									}
									break;
								}
							}
							break;
						}
					}
					if (!nextRowFound)
						throw new Exception ("Next state not found! The table is not closed!");
				}
			}

			return conj;
		}
		#endregion
		/// <summary>
		/// Constructor
		/// </summary>
		public L_Plus_M (IOracle_MAT_MM oracle)
		{
			myOracle = oracle;

			if (LibSetting.ConfOf ("AIDE.LPlusM.SaveConjectures") == "true")
				exportConj = true;
			else
				exportConj = false;

			if (LibSetting.ConfOf ("AIDE.LPlusM.SaveObsTables") == "true") {
				exportTables = true;
				//* the output format
				string oFormat = LibSetting.ConfOf ("AIDE.LPlusM.ExportTableFormat");
				switch (oFormat) {
				case "XML":
					exportFormat = ExportOptions.XML;
					break;
				case "HTML":
					exportFormat = ExportOptions.HTML;
					break;
				case "CSV":
					exportFormat = ExportOptions.CSV;
					break;
				default:
					exportFormat = ExportOptions.XML;
					Console.Write ("Wrong output is selected! XML is the default option.\n");
					break;
				}
			} else
				exportTables = false;

		}

		/// <summary>
		/// After adding a row into the Sm/Sm_I, we should fill the row with proper values
		/// </summary>
		/// <param name="tdr"></param>
		void UpdateTD_Row (TD_Row tdr)
		{
			for (int k = 0; k < tdr.Em_Row.Count; k++) {
				LearningLog.LogStartMQ ();
				Word output = myOracle.OutputTrace (tdr.accessString, Em [k]);
				LearningLog.LogFinishMQ ();

				tdr.Em_Row [k] = output.Suffix (Em [k].Length);
			}
		}

		/// <summary>
		/// Add a suffix to table
		/// </summary>
		/// <param name="suf"></param>
		protected void AddSuffixAndFillTable (Word suffix)
		{
			Em.Add (suffix);

			//* Fill the table for the resulsts of this newly added suffix
			foreach (TD_Row t1 in Sm) {
				LearningLog.LogStartMQ ();
				Word o = myOracle.OutputTrace (t1.accessString, suffix);
				Word myTree;
				//* to support output incompletness!
				if (o == null) {
					myTree = null;
				} else {
					myTree = o.Suffix (suffix.Length);
				}
				LearningLog.LogFinishMQ ();

				t1.Em_Row.Add (myTree);
			}
			foreach (TD_Row_Parrented t1 in Sm_I) {
				LearningLog.LogStartMQ ();
				
				Word o = myOracle.OutputTrace (t1.accessString, suffix);
				Word myTree;
				
				//* to support output incompletness!
				if (o == null)
					myTree = null;
				else
					myTree = o.Suffix (suffix.Length);
				LearningLog.LogFinishMQ ();

				t1.Em_Row.Add (myTree);
			}
		}

		/// <summary>
		/// look up for word <paramref name="p"/> in all entries of <paramref name="lst"/>
		/// </summary>
		/// <param name="lst"></param>
		/// <param name="path"></param>
		/// <returns></returns>
		protected int indexOfPath (List<TD_Row> lst, Word p)
		{
			for (int i = 0; i < lst.Count; i++) {
				if (lst [i].accessString.Equals (p))
					return i;
			}
			return -1;
		}

		/// <summary>
		/// look up for a word in all entries (path) of Sm_I
		/// </summary>
		/// <param name="lst"></param>
		/// <param name="path"></param>
		/// <returns></returns>
		protected int indexOfPath (List<TD_Row_Parrented> lst, Word p)
		{
			for (int i = 0; i < lst.Count; i++) {
				if (lst [i].accessString.Equals (p))
					return i;
			}
			return -1;
		}

		/// <summary>
		/// Based on Algorithm.3 (page 68) of Shahbaz PhD Thesis
		/// </summary>
		public virtual MealyMachine Learn ()
		{
			LearningLog.LogStartLearning ();
			InputAlphabet = myOracle.InputAlphabet;

			MealyMachine conj = null;
			phase = 0;

			//* initialize the observation table (Sm;Em; Tm) with the sets
			//* Sm = {epsilon}; Em = Sigma_i, SD.Sigma = {Epsilon.i} for all i in Sigma;
			//* ask the membership queries from (SD;ED; TD) ;
			//* update (SD;ED; TD) with the results of the queries ;
			InitializeObservationTable ();

			//* repeat until oracle replies yes to the conjecture MD 
			while (true) {

				#region Closedness

				bool tableIsClose = true;
				//* while (SD;ED; TD) is not closed myOracle not consistent do
				while (true) {
					//* if (SD;ED; TD) is not closed then 
					//*     find anotherRow in Sm.Sigma_i such that anotherRow ~(Em) input, for all input in Sm
					//*     move anotherRow to Sm
					//*     ask output queries for the extended table
					//* end

					int nc = isClosed ();
					tableIsClose = (nc == -1);
					if (tableIsClose)
						break;

					//* remove from Sm.Sigma AND add to Sm
					TD_Row t = Sm_I [nc];
					Sm_I.RemoveAt (nc);
					Sm.Add (t);
					int indexOfSym = 0;
					//* add anotherRow.a for each a in Sigma if they are not exist there
					foreach (ISymbol a in InputAlphabet.AllSymbols()) {
						
						//* to support output incompletness!
						indexOfSym++;						
						if (t.Em_Row [indexOfSym - 1] == null) {
							//* don't expand it!
							continue;
						}
						
						TD_Row_Parrented nt = new TD_Row_Parrented (t);
						nt.accessString.AddSymbol (a);

						//* don't add anotherRow if there is already one
						if (indexOfPath (Sm_I, nt.accessString) > -1)
							continue;
												
						Sm_I.Add (nt);
						FillRow(nt);
					}
				}

				#endregion

				//* add a potential suffix: if the table is not closed, try again to make it closed
				//if (AddPotentialSuffix ())
				//	continue;

				//* ask the equivalence query for MD 
				//* if oracle replies with a counterexample v then
				//*   add all the prefixes of v to SD
				//*   ask membership queries for the extended table
				//* end
				if (exportTables)
					ExportObservationTable ();
				
				conj = BuildConjecture ();
				conj.InputAlphabet = myOracle.InputAlphabet;
								
				
				//* save the conjecture
				if (exportConj)
					SMLib.Interoperability.DOT.DotHelper_MM.WriteToDot (
						LibSetting.WorkingPath + "Conjecture" + phase.ToString () + ".dot", conj);
				
				
				LearningLog.LogStartEQ ();
				Word counterexample = myOracle.EquivalenceQ (conj);
				LearningLog.LogFinishEQ ();

				phase++;
				//MealyUtils.DrawMealyMachine(conj);

				#region Process Counterexample

				//* Q: is there any counterexample?
				//* A: No! We found the RIGHT model => return the conjecture!
				if (counterexample == null) {
					LearningLog.LogFinishLearning ();
					return conj;
				}
				
				Console.WriteLine ("\n" + phase + ": Counterexample: " + counterexample);

				//* A: yes! find u.v where u is (the longest word) in (Sm Until Sm_I)
				int lengthOfU = 0;

				for (int i = 0; i < Sm.Count; i++) {
					int l = Sm [i].accessString.PrefixLength (counterexample);
					if (l > lengthOfU) {
						lengthOfU = l;
					}
				}

				for (int i = 0; i < Sm_I.Count; i++) {
					int l = Sm_I [i].accessString.PrefixLength (counterexample);
					if (l > lengthOfU) {
						lengthOfU = l;
					}
				}

				bool anyThingAdded = false;
				//* Then, add all suffix of v into Em
				for (int i = lengthOfU; i < counterexample.Length; i++) {
					Word pr = counterexample.Suffix (counterexample.Length - i);

					//* it is already in the Em
					if (Em.Contains (pr))
						continue;

					anyThingAdded = true;
                    
					//* Fill the table for the results of this newly added suffix
					AddSuffixAndFillTable (pr);

					if (isClosed () >= 0) {
						//* the table is already not closed!
						break;
					}
				}

				if (!anyThingAdded) {
					throw new Exception ("Something wrong happened!");
				}

				#endregion
			}
		}
	}
}
